行为时序逻辑中公平性的研究与完善

基于行为时序逻辑(TLA)的并发系统描述,就是对系统的初始状态、系统行为和行为的公平性进行规约和描述,但TLA中的公平性具有局限性,无法准确地描述某些系统的行为,从而限制了TLA的描述能力。通过研究TLA中公平性的推导过程,分析公平性的概念与定义方法,并以实际例子说明它的局限性。在此基础上,提出以加入两级新的公平性方式对其进行完善。最后,证明了新公平性等级之间的蕴涵关系。完善后的公平性具有更强的描述能力,能够对系统进行更完整的描述与规约。     

二次B-Spline时域基函数的TDFEM的应用

提出了时域有限元法(TDFEM)的一种新的基函数—二次B-spline时域基函数.首先简述了时域有限元法的原理和基本公式;然后提出了新型的基于B-spline函数的条件稳定和无条件稳定的时域有限元法方案,并应用于三维电磁辐射问题.通过典型的算例对这两种方案的精度、运算时间进行了比较,证实了基于二次B-spline函数的时域有限元法的有效性.通过稳定性理论分析得出该算法的精确稳定性,并且通过数值计算的结果得到验证.     

基于空时显著性感知的运动目标检测方法*

从视觉系统生理结构出发,对Itti视觉注意力模型进行了改进,融入运动特征,提出了一种基于视觉空时显著性感知的运动目标检测方法。首先提取图像的空间特征,形成空间显著图;然后利用相邻帧图像的全局运动、局部运动和相对运动,确定运动目标与背景的运动差异,形成运动显著图,并且对各显著区的空间特征和运动特征进行融合形成空时显著图,检测出运动目标。理论分析和实验结果表明,该方法能快速、准确地发现目标,减少目标的截获时间,提高目标跟踪性能。     

偏序时态模式下规范覆盖问题*

目前有效的多时间粒度时态数据库设计方法多针对全序时态模式,当时态模式的时态类型集为偏序集时,由于涉及时态类型间的最大下界等操作而使其难以实现。针对偏序时态模式的规范覆盖问题进行研究,提出了偏序TFD（时态函数依赖）集有限闭包、偏序模式属性集有限闭包、偏序无冗余覆盖和偏序规范TFD集等概念,解决了偏序TFD成员籍问题;并给出了偏序TFD集的规范覆盖算法,对其正确性进行了证明,对算法的时间复杂度进行了分析。为偏序时态模式的综合范式分解问题研究奠定基础。     

基于TLA的事件图模型形式化验证方法*

针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑(temporal logic of action,TLA)的事件图模型形式化验证方法.该方法利用TLA语言能够同时表达模型行为与逻辑规则的特点及其与事件图的相似性,将事件图模型及性质规约用TLA语言进行形式化描述,从而使该模型能够被TLA模型...     

并发系统中谓词行为图的行为时序逻辑表达

行为时序逻辑(TLA)组合时序逻辑与行为逻辑, 可以对并发系统进行描述与验证, 它引入动作和行为的概念, 使得系统和属性可用它的规约公式表示, 但存在用TLA描述复杂系统时TLA公式复杂且难以理解的不足。类似于状态转移图, 对于并发转移可以用谓词行为图进行图形化表示, 谓词行为图与行为时序逻辑规约具有相同的表达能力。介绍行为时序逻辑的语法、语义及简单推理规则, 用一个简单的实例说明使用谓词行为图去描述并发转移系统的有效性, 并用系统规约的TLA公式对谓词行为图表达能力进行证明, 表明两者具有等价性, 为描述和分析并发转换系统提供了一种可行的方法。     

近51年川中丘陵区的降水时空变化特征

为了提高雨水利用率,减少季节性干旱对四川省农业生产造成的影响,根据川中丘陵区9个气象站点1960~2010年的降雨资料,分别运用累计滤波器法和m-k秩次相关法定性和定量的描述了川中丘陵区降水变化趋势;从轮次和极差分析的角度揭示了降水丰、枯和持续性;基于morlet小波和降水集度探讨了该区降水在时间和空间上的稳定性。研究结果表明：川中丘陵区降水的m-k秩相关系数均小于0,降水总体呈下降趋势,但并不明显;降水集度和Hurst指数分别在11.6-14.2和0.54-0.79之间变化,降水呈季节性变化、持续性强;川中丘陵区降水具有5a、9a、21a左右的主周期,其中9a的周期振荡最强,降水时空变化较稳定。     

保持空间准确度与时间一致性的深度估计算法

为提高深度图的准确度,提出了一种基于图割的深度估计算法. 利用平均亮度 梯度联合匹配测度函数代替单像素亮度匹配,并考虑邻近像素深度相关性改变图割网络结构,提高深度估计的空间准确度;采用前一时刻同位置像素的深度约束当前时刻像素的深度值,使估计的深度图在时间上保持一致. 提出的算法考虑了深度图的空间、时间特征,可以提高深度图的准确度. 实验结果表明,与传统的基于图割的深度估计算法相比,新算法估计的深度图更加准确.     

Variability of complementary relationship and its mechanism on different time scales

In the complementary relationship (CR) between actual and potential evapotranspiration, wet envi- ronment evapotranspiration (Ew) is usually calculated using the Priestley-Taylor (P-T) equation. Based on the data obtained from 38 catchments of the Haihe River basin and the Weishan experiment site in Shandong Province of China, this study has found variations in the Priestley-Taylor parameter α (e.g. increase in values with increase in the amount of precipitation on annual scale, seasonal fluctuation noted t...     

基于ATSQL2时间点与时间段时态操作扩充

以时态数据操作语言ATSQL2为基础,对其时间点与时间段查询运算操作存在的不足进行扩充。增加时间运算操作函数,完成不同时态逻辑时间段运算,不同时间粒度之间的转换和时间比较逻辑判断操作。结果表明,扩充后的时间运算操作,丰富了原有ATSQL2的查询操作语义,简化了复杂时态数据操作语句的书写,使时态查询操作更加高效、简便。